(declare-fun sigmaStar_2 () String)
(declare-fun sigmaStar_3 () String)
(declare-fun literal_4 () String)
(declare-fun x_5 () String)
(declare-fun literal_6 () String)
(declare-fun x_7 () String)
(declare-fun x_8 () String)
(declare-fun literal_9 () String)
(declare-fun x_10 () String)
(assert (xor (= literal_9 "\u{22}\u{20}\u{2f}\u{3e}") (= x_5 (str.++ literal_4 sigmaStar_2))))
(assert (= (str.++ (str.++ x_7 sigmaStar_2) (str.++ x_5 literal_6)) (str.++ literal_4 (str.replace_all literal_9 sigmaStar_2 "\u{3c}\u{69}\u{6e}\u{70}\u{75}\u{74}\u{20}\u{74}\u{79}\u{70}\u{65}\u{3d}\u{22}\u{68}\u{69}\u{64}\u{64}\u{65}\u{6e}\u{22}\u{20}\u{6e}\u{61}\u{6d}\u{65}\u{3d}\u{22}"))))
(assert (str.< x_8 "\u{3c}\u{69}\u{6e}\u{70}\u{75}\u{74}\u{20}\u{74}\u{79}\u{70}\u{65}\u{3d}\u{22}\u{68}\u{69}\u{64}\u{64}\u{65}\u{6e}\u{22}\u{20}\u{6e}\u{61}\u{6d}\u{65}\u{3d}\u{22}"))
(assert (= x_7 (str.replace_all x_5 literal_6 "\u{22}\u{20}\u{76}\u{61}\u{6c}\u{75}\u{65}\u{3d}\u{22}")))
(assert (= (str.replace "\u{3c}\u{69}\u{6e}\u{70}\u{75}\u{74}\u{20}\u{74}\u{79}\u{70}\u{65}\u{3d}\u{22}\u{68}\u{69}\u{64}\u{64}\u{65}\u{6e}\u{22}\u{20}\u{6e}\u{61}\u{6d}\u{65}\u{3d}\u{22}" sigmaStar_2 (str.++ x_5 literal_6)) x_10))
(assert (= literal_9 "\u{22}\u{20}\u{2f}\u{3e}"))
(assert (= x_10 (str.++ (str.replace_all literal_4 sigmaStar_2 (str.++ x_7 sigmaStar_2)) literal_9)))
(assert (str.in_re x_10 (re.++ (re.* (re.diff (str.to_re "\u{5c}\u{3c}\u{53}\u{43}\u{52}\u{49}\u{50}\u{54}") (re.* re.allchar))) (re.++ (str.to_re "\u{5c}\u{3c}\u{53}\u{43}\u{52}\u{49}\u{50}\u{54}") (re.* re.allchar)))))
(check-sat)
